Definitions by Rewriting in the Calculus of Constructions
Identifieur interne : 005E34 ( Main/Exploration ); précédent : 005E33; suivant : 005E35Definitions by Rewriting in the Calculus of Constructions
Auteurs : Frederic BlanquiSource :
- Mathematical Structures in Computer Science ; 2005.
English descriptors
- KwdEn :
Abstract
This paper presents general syntactic conditions ensuring the strong normalization and the logical consistency of the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. On the one hand, the Calculus of Constructions is a powerful type system in which one can formalize the propositions and natural deduction proofs of higher-order logic. On the other hand, rewriting is a simple and powerful computation paradigm. The combination of both allows, among other things, to develop formal proofs with a reduced size and more automation compared with more traditional proof assistants. The main novelty is to consider a general form of rewriting at the predicate-level which generalizes the strong elimination of the Calculus of Inductive Constructions.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 003F93
- to stream Crin, to step Curation: 003F93
- to stream Crin, to step Checkpoint: 000282
- to stream Main, to step Merge: 006057
- to stream Main, to step Curation: 005E34
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="386">Definitions by Rewriting in the Calculus of Constructions</title></titleStmt><publicationStmt><idno type="RBID">CRIN:blanqui03a</idno><date when="2005" year="2005">2005</date><idno type="wicri:Area/Crin/Corpus">003F93</idno><idno type="wicri:Area/Crin/Curation">003F93</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">003F93</idno><idno type="wicri:Area/Crin/Checkpoint">000282</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000282</idno><idno type="wicri:Area/Main/Merge">006057</idno><idno type="wicri:Area/Main/Curation">005E34</idno><idno type="wicri:Area/Main/Exploration">005E34</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Definitions by Rewriting in the Calculus of Constructions</title><author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frederic" last="Blanqui">Frederic Blanqui</name></author></analytic><series><title level="j">Mathematical Structures in Computer Science</title><imprint><date when="2005" type="published">2005</date></imprint></series></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>lambda-calculus</term><term>rewriting</term><term>termination</term><term>typing</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="3628">This paper presents general syntactic conditions ensuring the strong normalization and the logical consistency of the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. On the one hand, the Calculus of Constructions is a powerful type system in which one can formalize the propositions and natural deduction proofs of higher-order logic. On the other hand, rewriting is a simple and powerful computation paradigm. The combination of both allows, among other things, to develop formal proofs with a reduced size and more automation compared with more traditional proof assistants. The main novelty is to consider a general form of rewriting at the predicate-level which generalizes the strong elimination of the Calculus of Inductive Constructions.</div></front></TEI><affiliations><list></list><tree><noCountry><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frederic" last="Blanqui">Frederic Blanqui</name></noCountry></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005E34 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005E34 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= CRIN:blanqui03a
|texte= Definitions by Rewriting in the Calculus of Constructions
}}
| This area was generated with Dilib version V0.6.33. |  |